$a$ =$_{b}$$s$,$t$ $b$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$(($a$.1) (=$_{b}$$s$) ($b$.1)) $\wedge_{b}$ (($a$.2) (=$_{b}$$t$) ($b$.2))